\documentclass[12pt,fleqn]{article}
%\usepackage[leftbars,dvips]{changebar}
%\usepackage[leftbars,pdflatex]{changebar}

\title{Victor: a SPARK VC Translator and Prover Driver \\[4ex]
  \Large
  User Manual for release 0.9.1 \\
  and subsequent experimental modifications \\[1ex]
% \normalsize
% \cbstart
%   \emph{Changebars indicate changes from User Manual for release 0.6 }\\[1ex]
% \cbend
%   \hbox{ }
} 

\author{Paul Jackson \\
        \texttt{pbj@inf.ed.ac.uk}}

\date{18 Feb 2013}

%\usepackage{vpage}
%\usepackage{vmargin}
%\setpapersize{Afour}

% margins l t r b, headheight, headsep, footheight, footskip
%\setmarginsrb{1.2in}{1.2in}{1.2in}{0.6in}{0.3in}{0.2inm}{0.3in}{0.3in}

\usepackage[a4paper,DIV14]{typearea} % LaTeX Companion, 2nd Ed, pp203-6
\usepackage{url}

\usepackage{array}

\setlength{\parindent}{0pt}

%My macros
%----------------------------------------------------------------------------
% Abbreviations
%----------------------------------------------------------------------------
\usepackage{amssymb}

\newcommand{\integer}{\ensuremath{\mathbf{Z}}}
\newcommand{\subrange}[2]{\{{#1}\:..\:{#2}\}}

\newcommand{\fixme}[1]{\textbf{FIXME: {#1}}}

\newcommand{\spark}{\textsc{Spark}}
\newcommand{\sparkb}{S{\footnotesize{}PARK}}  % for use in bold environments.
\newcommand{\ada}{Ada}
\newcommand{\sparkada}{SPARK-Ada}

\newcommand{\cvcthree}{\textsc{Cvc}3}
\newcommand{\cvcfour}{\textsc{Cvc}4}
\newcommand{\zthree}{\textsc{Z}3}
\newcommand{\yices}{Yices}
\newcommand{\altergo}{Alt-Ergo}

\newcommand{\blast}{\textsc{Blast}}
\newcommand{\slam}{\textsc{Slam}}

\newcommand{\sat}{\textsc{Sat}}
\newcommand{\smt}{\textsc{Smt}}
\newcommand{\smtb}{S{\footnotesize{}MT}}
\newcommand{\sal}{\textsc{Sal}}
\newcommand{\etb}{\textsc{Etb}}

\newcommand{\sri}{\textsc{Sri}}
\newcommand{\smtlib}{\textsc{smt-lib}}

\newcommand{\fdl}{\textsc{Fdl}}
\newcommand{\rls}{\textsc{rls}}
\newcommand{\rlu}{\textsc{rlu}}
\newcommand{\vcg}{\textsc{vcg}}
\newcommand{\siv}{\textsc{siv}}

%NB the extensions here changed in V0.9, for SPARK tool compatibility
\newcommand{\logfile}{\textsc{vlg}}
\newcommand{\goalreportfile}{\textsc{vct}}
\newcommand{\unitsumfile}{\textsc{vus}}
\newcommand{\sessionsumfile}{\textsc{vsm}}

\newcommand{\csv}{\textsc{csv}}

%\renewcommand{\And}{\ensuremath{\wedge}}
\newcommand{\And}{\ensuremath{\wedge}}
\newcommand{\Not}{\ensuremath{\neg}}
\newcommand{\Or}{\ensuremath{\vee}}
\newcommand{\Iff}{\ensuremath{\Leftrightarrow}}
\newcommand{\Implies}{\ensuremath{\Rightarrow}}

\newcommand{\tttilde}{{\tt \char`\~}}
\newcommand{\ttstar}{{\tt \char`\*}}
\newcommand{\ttqmark}{{\tt \char`\?}}


% Boolean option with short one-line description
\newcommand{\optionbs}[1]{\item[\texttt{-{#1}}]}
% Boolean option with long description
\newcommand{\optionb}[1]{\item[\texttt{-{#1}}]\ \\}
% Value option
\newcommand{\optionv}[2]{\item[\texttt{-{#1}=}\mdseries\textit{#2}]\ \\}


%----------------------------------------------------------------------------
% Draft support
%----------------------------------------------------------------------------
\usepackage{comment}

\specialcomment{outline}%
  {\begingroup\bfseries\slshape\begin{itemize}}%
  {\end{itemize}\endgroup}


\specialcomment{question}%
  {\begin{itemize}\item[\Huge \textbf{?}]\itshape}%
  {\end{itemize}}

\specialcomment{remark}%
  {\begin{itemize}\item[\Huge \textbf{!}]\itshape}%
  {\end{itemize}}

% \excludecomment{outline}
% \excludecomment{question}
% \excludecomment{remark}

\newcommand{\todo}[1]{\textbf{ToDo:} \emph{#1}}
%\newcommand{\todo}[1]{\emph{\bfseries{#1}}}

\newenvironment{todoenv}{\begingroup\itshape}{\endgroup}



\usepackage[colorlinks=true]{hyperref}

\begin{document}

\maketitle

%\begin{abstract}
%This is a user guide for V0.8.
%\end{abstract}

\tableofcontents


\setlength{\parskip}{0.8\baselineskip}

%============================================================================
%\section{Introduction}
%============================================================================

%============================================================================
\section{Supported provers and prover languages}
%============================================================================

Victor has API interfaces to the \cvcthree{} and \yices{} provers, and
can drive any prover that accepts Simplify, \smtlib{} v1.2 or
\smtlib{} v2 format input files.

%----------------------------------------------------------------------------
\subsection{Simplify language}
%----------------------------------------------------------------------------

The Simplify language is supported by the Simplify and \zthree{} provers.

%----------------------------------------------------------------------------
\subsection{SMT-LIB languages}
%----------------------------------------------------------------------------

The \smtlib{} initiative (\url{http://www.smtlib.org}) defines
standard languages for formatting input to \smt{} solvers and collects
benchmarks in this format. Victor supports the current version 2.0
and the older version 1.2.

The initiative defines particular \emph{logics}, each characterised by
some combination of logical theories and possible restrictions on
shapes of terms and formulas.  These logics are used to classify
benchmarks, and different \smt{} solvers support different logics.
Some solvers support a superset of what is defined by any of these
logics.

At a minimum, Victor requires solvers to handle uninterpreted
functions and constants, linear integer arithmetic and logical
quantifiers.

The following logics in both v1.2 and v2.0 provide at least this support:
\begin{itemize}
\item \textsc{auflia}: quantifier formulas involving arrays,
  uninterpreted functions, linear integer arithmetic.
\item \textsc{auflira}: quantifier formulas involving arrays,
  uninterpreted functions, linear integer and linear real arithmetic.
\item \textsc{aufnira}: quantifier formulas involving arrays,
  uninterpreted functions, non-linear integer and non-linear real
  arithmetic.
\item 
\textsc{ufnia}: Non-linear integer arithmetic with uninterpreted
  sort, function, and predicate symbols.
\end{itemize}
Victor can also take advantage of support for real arithmetic and for
sort symbols.  Such provers include Alt-Ergo, \cvcthree, \cvcfour,
\yices{} and \zthree.
% Victor currently makes no use of the support for arrays
% provided by the above logics or by prover-specific
% extensions.

One major benefit of v2.0 is better support for queries involving
mixed real and integer arithmetic.  Victor does translate real
arithmetic to v1.2 of the \smtlib{} format. However, v1.2 does not
support well goals in which integers and reals are mixed. (For
example, it does not define a function injecting the integers into the
reals.)
  

%----------------------------------------------------------------------------
\subsection{Alt-Ergo}
%----------------------------------------------------------------------------

Alt-Ergo is an open-source \smt{} solver from LRI (Laboratoire de
Recherche en Informatique) at Universit\'e Paris-Sud.  It is available
from \url{http://alt-ergo.lri.fr/}.

Victor has been tested most recently with the v0.95 release (11th Jan
2013) using Alt-Ergo's \smtlib{} 1.2 and 2.0 file-level interfaces.
Alt-Ergo's 1.2 interface works fine, but issues have been noted with
the 2.0 interface in both the v0.94 and v0.95 releases.
\begin{enumerate}
\item \texttt{define-type} is not supported.
\item \texttt{to\_real} function is not recognised.
\item Instances of quantified Bool-typed variables are 
  not recognised when they occur in formula positions. 
  For example, it rejects
\begin{verbatim}
  (assert (forall ((x Bool)) x))
\end{verbatim}
  though it accepts
\begin{verbatim}
  (assert (forall ((x Bool)) (= x x)))
\end{verbatim}

\item Boolean operators (`and', `or', etc.) are not recognised when
  they occur in term positions. For example, it rejects
\begin{verbatim}
  (declare-fun F (Bool) Bool)
  (assert (F (and true true)))
\end{verbatim}
\end{enumerate}
Victor has full work-arounds for 1, 3 and 4 and a partial work-around
for 2.  For 2, it replaces instances of \texttt{to\_real} with an
uninterpreted function.  Axiomatisation of the properties of
\texttt{to\_real} has not yet been explored.

Alt-Ergo's output is also not fully compliant with both the 1.2 and
2.0 standards: it will output the non-standard \verb+unknown (sat)+
rather than simply \verb+sat+, and output multiple \texttt{unsat}
responses to a single satisfiability check request.  Victor has
work-arounds so it tolerates these non-standard issues.

The v0.95 release is preferred over the v0.93 and v0.94 releases as
both v0.93 and v0.94 sometimes has been observed to have fatal errors,
whereas no such errors have been observed yet with v0.95.
%\verb+Fatal error: exception Exception.Unsolvable+

% If the standalone Alt-Ergo executable is downloaded rather than built
% from the Alt-Ergo source distribution, it is also necessary to copy
% the file \texttt{smt\_prelude.mlw} from the source distribution to the
% \texttt{run/} directory.


%----------------------------------------------------------------------------
\subsection{CVC3}
%----------------------------------------------------------------------------

\cvcthree{} is an open-source \smt{} solver jointly developed at New
York University and the University of Iowa.  It is available from
\url{http://www.cs.nyu.edu/acsys/cvc3/}.

Victor can link to a \cvcthree{} library and can then drive
\cvcthree{} via its API.  Alternatively Victor can invoke a
\cvcthree{} stand-alone executable on \smtlib{} format files.

Victor has been tested with the last release, V2.4.1, dating from
September 2011.
%
% The \cvcthree{} developers also make available daily
% development releases.  Victor has not yet been tested with these.
%
\cvcthree{} is significantly slower than \yices{} or \zthree{} (maybe
5-10$\times$), especially when VCs are unprovable. 
%
It has some basic support for non-linear arithmetic.

The API interface of this version is essentially unusable by Victor,
as, on some goals, the \cvcthree{} code ignores the request for it to
return after a set timeout period.  When this happens, Victor itself
is just stuck and cannot progress on to other goals.

% When driven via its API, this version of \cvcthree{} throws exceptions
% and has some segmentation faults on a few of the \spark{} VCs from the
% tokeneer set,
% %
% The exceptions are caught and reported by Victor, but 
% %
% the segmentation faults cause Victor to halt.  To enable Victor runs
% in the presence of these faulting problems, it is possible to tell
% Victor to ignore trying to run \cvcthree{} on certain VCs.  

%----------------------------------------------------------------------------
\subsection{CVC4}
%----------------------------------------------------------------------------
\cvcfour{} is a successor to \cvcthree, developed by the same team.
It is available from \url{http://cvc4.cs.nyu.edu}.

Victor has been tested with the first release, V1.0, made on 3rd December 2012, 
using the the \smtlib{} 1.2 and 2.0 file-level interfaces.  Currently there
is no API interface to \cvcfour.

While \cvcfour{} does not support the \verb+to_real+ operator in mixed
integer real \smtlib{} 2 logics, it does seem to allow implicit
integer to real conversion which achieves much the same end.

%----------------------------------------------------------------------------
\subsection{Simplify}
%----------------------------------------------------------------------------

Simplify is a legacy prover, used most notably in the ESC/Java tool. 

The Modula-3 sources and some documentation are available from HP labs.
Visit \url{http://www.hpl.hp.com/downloads/crl/jtk/index.html} and follow
the ``Download Simplify here'' link.

Executables for Linux and other platforms can be pulled out of the
ESC/Java2 distribution: visit
\url{http://secure.ucd.ie/products/opensource/ESCJava2/}.
In October 2007, the executables for V1.5.4 were found in a file 
\texttt{Simplify-1.5.5-13-06-07-binary.zip}.  These are 32-bit executables.
No success has been found in locating any 64-bit executables. 

Simplify has good performance, but is unsound and sometimes crashes
because it uses fixed-precision integer arithmetic.

Victor interfaces to Simplify using temporary files and by invoking
the Simplify executable in a sub-process.  Unlike the case with
\cvcthree{}, Victor can tolerate Simplify crashing.  Victor provides
notifications of Simplify crashes in its output files.


%----------------------------------------------------------------------------
\subsection{Yices}
%----------------------------------------------------------------------------

\yices{} is a state-of-the-art \smt{} solver available from \sri{} at
\url{http://yices.csl.sri.com/}.

Victor links with a \yices{} library provided with the \yices{}
distribution.  Victor has been tested with the latest public release,
V1.0.37 (Jaunary 2013).  This version, bug fixes apart, dates from
summer 2007 and essentially is the version that led the field in the
2007 \smt{} competition.

% \yices{} 1 is no longer under development: \sri{} is
% currently working on a re-implementation, \yices{} 2, which had a
% preliminary showing at the 2008 \smt{} competition.  \yices{} 2 is not
% currently available, and 

\yices{} is fussy about VCs containing non-linear arithmetic
expressions.  Victor currently just has \yices{} ignore any hypotheses
or conclusions containing such expressions, and, not infrequently, VCs
are provable despite these ignored VC clauses.  
%

\yices{} will accept universally-quantified hypotheses with non-linear
arithmetic expressions, and sometimes can make use of linear
instantiations of these.
%
Unfortunately, the current behaviour on finding a non-linear
instantiation is abandon the proof attempt rather than simply ignore
the instantiation.  

No crashes have been observed with recent versions of \yices.
However, on a few VCs (not in the test sets provided with the
distribution), \yices{} just keeps going on and on.  No mechanism for
timing out on such cases has yet been implemented, the only way to
deal with them is to request that Victor ignore them.

Victor can also drive Yices using \smtlib{} 1.2 format files. In this
case all arithmetic must be linear -- non-linear arithmetic operators
have to be abstracted to uninterpreted functions.

A successor solver Yices 2 is available.  The latest version is 2.1.0,
released August 2013.  This version is unsuitable for use as it does
not support quantifiers.

%----------------------------------------------------------------------------
\subsection{Z3}
%----------------------------------------------------------------------------

\zthree{} is a state-of-the-art \smt{} solver developed at Microsoft. See
\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}.

Victor has been tested most recently with the Linux version of release
4.3.1, made on 12th Nov 2012.  No problems have been observed with
this version.

% This website only provides a Windows version of a Z3 executable.
% Microsoft research staff have verbally advertised the existence of a
% Linux version.  Victor has been tested with such a version (V1.3),
% obtained from Leonardo de Moura, \texttt{leonardo@microsoft.com}, one
% of \zthree's developers.

\zthree{} has good performance and better VC coverage than other
solvers tried.  In particular, it has the best support for non-linear
arithmetic.

Victor interfaces to \zthree{} using temporary files and by invoking
the \zthree{} executable in a sub-process.  The temporary files can be
in \smtlib{} 1.2, \smtlib{} 2.0 or Simplify format.

% Despite the similarity of the format, \zthree's performance can be radically
% different, depending on the format: it seems that \zthree{} has a soft
% timeout of under 0.1s when taking Simplify format input, but no such timeout
% on \smtlib{} format input.

%============================================================================
\section{Installation and Testing}
%============================================================================

Victor is written in C++ and currently only runs on Linux.  The
current distribution includes some preliminary code to allow it to
compile and run on Windows.  However, this code has not yet been fully
tested.

At Edinburgh, Victor is currently compiled and run on a Scientific
Linux 6 64-bit platform. Scientific Linux 6 is based on Red Hat
Enterprise Linux 6.  It makes use of the following tools:
\begin{itemize}
\item \texttt{make} V3.81
\item \texttt{gcc/g++} V4.4.5
\item \texttt{bison}  V2.4.1
\item \texttt{flex} V2.5.35
\end{itemize}
% For SL5:
% \begin{itemize}
% \item \texttt{make} V3.81
% \item \texttt{gcc/g++} V4.1.2
% \item \texttt{bison}  V2.3
% \item \texttt{flex} V2.5.4
% \end{itemize}
The main external library it uses is
\begin{itemize}
\item \texttt{gmp} V4.3.1
%\item \texttt{gmp} V4.1.4
\end{itemize}
Its precise dependencies on these versions are largely unknown. 
%
One observation is that some tweaks to the \texttt{bison code} in
\texttt{parser.yy} were necessary when shifting from \texttt{bison}
V2.3 to \texttt{bison} V2.4.  Comments in \texttt{parser.yy} indicate
what needs to be changed for compilation with V2.3

By default, the \texttt{gmp} library is dynamically linked in.  If
running a single executable on several different Linux platforms, this
can cause problems and it might be desirable to use static linking
instead.  To achieve this, use \texttt{STATIC\_GMP=true} on the
\texttt{make} command line when building Victor.

To install:
\begin{enumerate}
\item Untar the distribution.  E.g. 
\begin{verbatim}
  tar xzf vct-0.9.0.tgz
\end{verbatim}
  This should generate a top level directory
  \texttt{vct-0.9.0} including subdirectories 
    \texttt{src},
    \texttt{bin},
    \texttt{run},
    \texttt{vc}
   and \texttt{doc}.
   The \texttt{doc} directory includes a copy of this manual.
   Other directories are described below.
\item 
  Configure Victor for each of the provers you wish to use it with.
  \begin{description}

  \item[\cvcthree:] To enable the API driver, uncomment the definition
    of variable \texttt{CVC3DIR} in file \texttt{src/Makefile} and edit
    its value to be that of your \cvcthree{} installation.  
    
    To use the \smtlib{} format file interface, ensure that an
    executable \texttt{cvc3} is on your current path.

  \item[Simplify:] Ensure an executable called \texttt{simplify} is on your
    current path. 

  \item[\yices:] 
    To enable the API driver, uncomment the definition of variable
    \texttt{YICESDIR} in file \texttt{src/Makefile}, and edit its
    value to be that of your \yices{} installation.

    To use the \smtlib{} format file interface, ensure that an
    executable \texttt{yices} is on your current path.

  \item[\zthree:]  Ensure an executable called \texttt{z3} is on your
    current path.

  \item[\altergo:]  Ensure an executable called \texttt{alt-ergo} is on your
    current path.
  \end{description}
  Alternate names, and optional paths can be specified for each executable
  at the top of the \texttt{Makefile} in the \texttt{run} directory.

  Victor can be run without driving any prover.  This is useful for
  testing if Victor's parser can handle certain VCs and for gathering
  information on VCs.  This mode can be used for compiling reports on
  the coverage obtained with the Simplifier prover provided with
  Praxis's \spark{} toolkit.

\item Build a Victor executable by \texttt{cd}ing to the \texttt{src}
  directory and typing \texttt{make}.  This does a variety of things, including
  \begin{enumerate}
  \item Creating \texttt{.d} files recording \texttt{make} rules that
     capture dependencies between source files.
   \item Running the \texttt{bison} parser generator and the \texttt{flex}
     lexer generator.
   \item Compiling various \texttt{.o} files.
   \item Linking the \texttt{.o} files together, along with prover
     libraries and the \texttt{gmp} library, and installing the
     resulting executable named \texttt{vct} in the \texttt{bin}
     directory.
  \end{enumerate}
  For convenience, a sub-directory \texttt{build} contains copies
  of files created during a build of Victor where it was configured
  for running with the Simplify and \zthree{} provers.  For example, if you
  do not have the correct version of \texttt{bison}, you could copy over
  the \texttt{bison} output files to the \texttt{src} directory.


\item Add the \texttt{vct/bin} directory to your \texttt{PATH}.
%  if you
%   wish to run Victor without specifying the path to this \texttt{bin}
%   directory.


\item Build utility tools for analysing the \goalreportfile{},
  \unitsumfile{} and \sessionsumfile{} comma-separated-value output
  files created by Victor.  Enter \texttt{make csvutils}.  This causes
  the executables \texttt{csvproj}, \texttt{csvfilt},
  \texttt{csvmerge} and \texttt{csvisect} to be added to the
  \texttt{bin} directory.

\item Build an auxiliary program for timing-out runs of provers.
  Enter \texttt{make watchdog}.  This creates the executable
  \texttt{run/watchdogrun}.

\item Try running Victor on the example VCs provided with the distribution.
  Check the output files match the provided output files.  See Section
  \ref{sec:examples}
  for details.
\end{enumerate}

%============================================================================
\section{Operation}
%============================================================================
%----------------------------------------------------------------------------
\subsection{Terminology}
%----------------------------------------------------------------------------
We refer to \spark{} VCs as \emph{goals} and use the term \emph{goal
  slice} to refer to a proof obligation build from a VC by considering
just one of the goal's conclusions and ignoring the others.  
%
For brevity, we sometimes collectively refer to \spark{} VC goals and
slices of \spark{} VC goals as \emph{Victor goals} or even just
\emph{goals}.

A \emph{unit name} is the hierarchical name of a program unit.  The unit
name with a \texttt{.fdl}, 
\texttt{.rls}, 
\texttt{.vcg} or 
\texttt{.siv} suffix gives a pathname for the corresponding
VC file relative to the root directory of all the VC files for a \spark{}
program.

%----------------------------------------------------------------------------
\subsection{Basic operation}
%----------------------------------------------------------------------------


The basic operation of Victor is to 
\begin{enumerate}
\item Read in a list of names of \spark{} program units.

\item For each program unit
  \begin{enumerate}
  \item Read in the VCs described in the \texttt{.fdl}, \texttt{.rls},
  \texttt{.vcg} file triples output by the \spark{} Examiner for the
  unit.\footnote{
  Optionally it can read in the simplified
  \texttt{.siv} files output by the \spark{} Simplifier instead of the 
  \texttt{.vcg} files.}
  \item Invoke a prover on each goal or goal slice. 
  \item Output \texttt{.vct}, \texttt{.vus}, \texttt{.vsm} and
    \texttt{.vlg} report files.
  \end{enumerate}
\end{enumerate}

%----------------------------------------------------------------------------
\subsection{Input and output files}
%----------------------------------------------------------------------------
The Victor-specific input and output files are as follows.

% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\subsubsection{Unit listing input file}
% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\label{sec:unit-listing-file}

Typically Victor is run on many program units at once.  An input
\emph{unit listing} \texttt{.lis} file is used to indicate the units
it should consider.  
%
The grammar for each line in a unit listing file is given by

\noindent
\begin{tabular}{lll}
\textit{line}  & ::= & \textit{unitname} \{\textit{option}\}  \\[2ex]
%
\textit{option} & ::= & [\textit{tag}\texttt{?}]\textit{val} \\[2ex]
%
\textit{val} & ::= &  \textit{goal} \\
    & $|$  &  \textit{goal}\texttt{.}\textit{concl} \\
    & $|$  &  \textit{filename}\texttt{.fdl} \\
    & $|$  &  \textit{filename}\texttt{.rul} \\
    & $|$  &  \textit{filename}\texttt{.rlu} 
\end{tabular}

\noindent
where square braces ([]) enclose optional non-terminals,
curly braces (\{\}) enclose non-terminals repeated 0 or more times,
%
the terminals \textit{unitname}, \textit{tag} and \textit{filename} are
alphanumeric strings, 
and the terminals \textit{goal} and \textit{concl} are natural numbers.
%
The meaning of the components of a line are as follows.
\begin{itemize}
\item \textit{unitname} is the hierarchical name of a unit (\spark{}
  subprogram).

\item \textit{tag} tags an option.  A tagged option is only active if
  the tag is also supplied as one of the values of the 
  \texttt{-active-unit-tags} Victor command-line option.
  Untagged options are always active.

\item \textit{goal} and \textit{goal}\texttt{.}\textit{concl} 
  select particular goals and goal slices in the unit. 
  The Victor command-line options 
  \texttt{-include-selected-goals} and
  \texttt{-exclude-selected-goals}
  control how Victor treats these selected goals and goal slices.

\item \textit{filename}\texttt{.rul} and
      \textit{filename}\texttt{.rlu} are auxiliary rules files to load

\item \textit{filename}\texttt{.fdl} is an auxiliary declarations file.
  For example, this can declare constants and functions introduced in 
  an auxiliary rules file.
\end{itemize}
Comment lines are allowed: these are indicated by a \texttt{\#}
character in the first column.  Also blank lines are allowed.  

One way to prepare a unit listing file is to run the command
\begin{verbatim}
  find . -name '*.fdl' | sed -r 's/\.\/|\.fdl//g' > units.lis
\end{verbatim}
in the root directory of a set of VC files.


% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\subsubsection{Goal report (VCT) output file}
% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

The goal report or \goalreportfile{} file has suffix \texttt{.vct}.  

The file is in comma-separated-value (\csv) format: linebreaks divide the file
into records, and each record is divided by commas into fields.  Field values in
general might contain commas and linebreaks, in which case the field value is
enclosed in \texttt{""}s.

Each record gives information on one Victor goal.
The record fields are:
\begin{enumerate}
\item Unit number.  The number of the unit the goal is from.  Victor numbers
   the units it reads sequentially, starting from 1.
\item Path to unit. This describes the containing packages.
\item Unit name, without a prefix for the containing packages.
\item Unit kind.  One of \texttt{procedure}, 
  \texttt{function} or \texttt{task\_type}.
\item Goal origins information -- source of path in subprogram for VC .
\item Goal origins information -- destination of path for VC, or VC
  kind if not path related.
\item VC goal number.
\item Conclusion (goal slice) number.  Empty if the Victor goal is generated
   form the whole \spark{} goal.
 \item Status (one of \texttt{trivial}, \texttt{true}, \texttt{unproven} or
   \texttt{error}).
\item Proof time (in sec).
\item Brief remarks about goal and solver interactions
\item Operator kinds occurring in hypotheses
\item Operator kinds occurring in conclusion
\end{enumerate}
A file \texttt{vct-file-header.txt} provides a 1 line comma-separated
list of field headings for these goal report files.  By default, the
\goalreportfile{} files are generated without this heading.



% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\subsubsection{Unit summary (VUS)  output file}
% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
The unit summary or \unitsumfile{} file has suffix \texttt{.vus} and is
in \csv{} format.
Each record gives a summary of the Victor run on one unit.
The record fields are:
\begin{enumerate}

% Identity of unit
\item Unit number.
\item Unit name, including prefix showing containing packages

% Health of run
\item Number of \texttt{ERROR} messages written to \logfile{} log file.
\item Number of \texttt{WARNING} messages written to \logfile{} log file.

% Outcome of runs on goals
\item Total number of goals.
\item Number of trivial goals.
\item Number of goals found true by the prover.
\item Number of goals unproven by the prover.
\item Number of unproven goals where the prover timed out.
\item Number of unproven goals where the prover asserted the goal was
  definitely false.
\item Number of goals where some error occurred in handling the goal

% User rule stats
\item Number of user rules read in from the directory-level and unit-level
  user rule (\texttt{.rlu}) files.
\item Number of directory-level user rules excluded because of unbound
  function, constant or type ids, or because they do no not type check.
\item Number of unit-level user rules excluded.
\item Number of system rules excluded, (\emph{system rules} being rules
  generated by the Examiner or provided by Victor).

% AST stats
\item Size of combined parse tree for unit input files.
\item Size of abstract syntax tree after all prover-independent
  translation steps in Victor.
\item Number of abstract syntax tree nodes allocated for unit

% Times
\item Total time to handle unit
\item Total time in prover when proof succeeded.
\item Average time in single prover run when proof succeeded.
\item Maximum  time in single prover run when proof succeeded.
\item Total time in prover when proof failed.

% Rule auditing stats
\item Whether unit is inconsistent, when all user rules and all
  hypotheses and conclusions of specific goals are ignored.  Value is
  1 if inconsistent, otherwise 0.
\item Whether unit is inconsistent, when all user rules considered,
  but all hypotheses and conclusions of specific goals are ignored.
  Value is 1 if inconsistent, otherwise 0.
\item Number of user rules found to be inconsistent with system-supplied rules
  and built-in theories of the prover. 
\item Number of user rules found to be derivable from system-supplied rules
  and built-in theories of the prover. 
\item Number of user rules found to be derivable from other user
  rules, along with system-supplied rules and built-in theories of
  the prover.

% Remarks
\item Remarks on unit generated by Victor
\end{enumerate}
A file \texttt{vus-file-header.txt} provides a 1 line comma-separated
list of field headings for these unit summary files.  By default, the
\unitsumfile{} files are generated with this heading to simplify
reading the files in a spreadsheet program.


% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\subsubsection{Session summary (VSM) output file}
% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
The session summary or \sessionsumfile{} file has suffix \texttt{.vsm} and is
in \csv{} format.  It contains one record summarising a Victor run over one
or more units.
The record fields are:
\begin{enumerate}
\item Report file name with any of the suffices.

% Health of session
\item Number of \texttt{ERROR} messages in log file
\item Number of \texttt{WARNING} messages in log file

% Outcomes
\item Total number of goal/goal slices processed.
\item Number of goals with \emph{true} status
\item Number of goals with \emph{unproven} status
\item Number of unproven goals that involved a timeout.
\item Number of unproven goals that were shown to be definitely false.
\item Number of goals with \emph{error} status

% Outcome percent stats
\item Percent of goals with \emph{true} status
\item Percent of goals with \emph{unproven} status
\item Percent of goals that were unproven and involved a timeout.
\item Percent of goals that were shown false.
\item Percent of goals with \emph{error} status

% Times
\item Total time to handle all units of session
\item Total time in prover when proof succeeded.
\item Average time in single prover run when proof succeeded.
\item Maximum  time in single prover run when proof succeeded.
\item Total time in prover when proof failed.

% Rule auditing stats
\item Number of inconsistent units, when all user rules and all
  hypotheses and conclusions of specific goals are ignored.  Value is
  1 if inconsistent, otherwise 0.
\item Number of inconsistent units, when all user rules considered,
  but all hypotheses and conclusions of specific goals are ignored.
  Value is 1 if inconsistent, otherwise 0.
\item Number of user rules found to be inconsistent with system-supplied rules
  and built-in theories of the prover. 
\item Number of user rules found to be derivable from system-supplied rules
  and built-in theories of the prover. 
\item Number of user rules found to be derivable from other user
  rules, along with system-supplied rules and built-in theories of
  the prover.

\end{enumerate}
A file \texttt{vsm-file-header.txt} provides a 1 line comma-separated list
of headings for these summary files.

Summary files can be concatenated together with the header file and then 
viewed in any spreadsheet program.

% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
\subsubsection{VLG output file}
% - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
The \logfile{} log file includes
\begin{enumerate}
\item a record of the command line options passed to Victor,
\item various information, warning and error messages,
\item user rule analysis reports,
\item statistics on the run, including numbers of VCs proven and unproven,
  and time taken.
\end{enumerate}

%----------------------------------------------------------------------------
\subsection{Invocation of Victor}
%----------------------------------------------------------------------------
The command line syntax for invoking Victor is
\begin{quote}
  \texttt{vct} [\textit{options}] [\textit{unitname}] 
\end{quote}
The \textit{unitname} argument is used to identify a single unit on which 
to run Victor.

To run Victor on multiple units, omit the \texttt{unitname} argument
and use instead the \texttt{units} option to specify a unit listing
input file.

If both a \textit{unitname} and a \texttt{units} option are provided,
the \texttt{units} option is ignored.

Victor takes numerous options, many of which are currently necessary.
See the next section for a description of a \texttt{Makefile} that
provides standard option sets.


%----------------------------------------------------------------------------
\subsection{Examples}
%----------------------------------------------------------------------------
\label{sec:examples}

The \texttt{vc} directory has subdirectories for some example 
sets of VCs.
%  that
% Victor has so far been tested on.
% \begingroup
% \renewcommand{\descriptionlabel}[1]{\texttt{#1}}
% \begin{description}
% \item[autop] The autopilot example distributed with the 
%   \spark{} book: ``High Integrity Software: The \spark{} Approach to 
%    Safety and Security'' by John Barnes.

% \item[hilton] Adrian Hilton's SPARK Missile Guidance Simulator.
% \item[tokeneer] The Tokeneer ID station case study prepared by Praxis
%   for the NSA.
% \end{description}
% \endgroup
See the file \texttt{vc/README.txt} for further information on these sets.
% sources of these VC sets.

The \texttt{run} directory provides a Makefile with rules for
running Victor on the VC sets in the \texttt{vc} directory.
%
These rules use Make patterns in their targets, and can easily also be
used for running Victor on users' own VC sets.
%
The rules set appropriate Victor command-line options and so allow
starting Victor users to ignore having to figure these out for
themselves.
%
See \texttt{run/Makefile} for details.

Reference report files obtained from running \texttt{make} on some of
these targets are included in directory \texttt{run/out-ref}.
%
Unix \texttt{diff} can be used to check that newly-generated
report files are the same as the reference files.
%
If the command line option \texttt{-gstime} is used to include times
of prover runs in report files, it will be necessary to use
the \texttt{csvproj} utility to remove the field for these times
in order to get files that are expected to be identical.

%----------------------------------------------------------------------------
\subsection{Performance tips}
%----------------------------------------------------------------------------

\begin{enumerate}

\item When \smt{} solvers cannot prove a goal, they often keep trying
  almost indefinitely rather than halting, so it is good to run them
  with some kind of time-out.  
  %
  When several VCs cannot be proven, Victor's total run-time can be
  dominated by the runs that go to time-out.  Setting a shorter
  time-out can therefore sometimes radically reduce Victor's run-time,
  often with little or no drop in number of goals proven.

\item \smt{} solver performance on goals they can prove is often
  dependent on the number of quantified axioms. 
  By default, Victor uses a number of quantified axioms from the 
  rules files \texttt{divmod.rul} and \texttt{prelude.rul} in the \texttt{run/}
  directory. 
  %
  In some cases, not all these axioms are necessary, and faster
  run-times are achievable with alternate rules files that prune down
  these axiom sets.

\end{enumerate}


%============================================================================
\section{Command line options}
%============================================================================
Options are specified with syntax 
\texttt{-\emph{name}} or
\texttt{-\emph{name}=\emph{value}}.
%
Option values can be boolean (\texttt{true} or \texttt{false}),
natural numbers (e.g. \texttt{42}) or strings.
%
An option \texttt{-\emph{name}} is interpreted the same as 
an option \texttt{-\emph{name}=true}.  An unset boolean option is interpreted
as \texttt{-\emph{name}=false}.

If the same option is given multiple times with different values, the
usual behaviour is that the last value is taken.  Occasionally all multiple 
values are used.  These cases are always explicitly pointed out below.

A later option 
\texttt{-name=},
\texttt{-name=false},
\texttt{-name=none} or 
\texttt{-name=default}
clears all earlier values given for the option and makes it unset.

%----------------------------------------------------------------------------
\subsection{Input options}
%----------------------------------------------------------------------------

These options control where VCs are read from, provision of auxiliary
declarations and rules, and filtering of VCs before invoking the selected
prover.

\begin{description}

  \optionv{units}{unit-listing}  Run on units named in \textit{unit-listing}
   file.

  \optionv{prefix}{prefix} 
    Use \textit{prefix} as a common prefix for all unit names.  
    \textit{prefix}\texttt{/}\textit{unitname} should give an absolute or
    relative pathname for the VC file set of a program unit.  Default is
    that no prefix is used.
   
  \optionv{decls}{declfile}
    For every program unit, read auxiliary \texttt{.fdl} 
    declarations file named in \textit{declfile}.  
    Multiple files can be specified using multiple 
    \texttt{-decls} options.
%     For example, the Examiner does not provide declarations for built-in
%     bit operations such as \texttt{bit\_\_or} and \texttt{bit\_\_not}.

  \optionb{read-all-decl-files-in-dir}
  For each program unit with full name \textit{dirs/dir/unitname},
  read in all \fdl{} declaration files in directory \textit{dirs/dir/} rather
  than just the \fdl{} declaration file \textit{dirs/dir/unitname.fdl}.
  This option is useful in conjunction with 
  \texttt{-read-directory-rlu-files}
  and \texttt{-read-unit-rlu-files} when the user-defined rules files for a
  unit 
  (see options \texttt{-read-directory-rlu-files} 
   and \texttt{-read-unit-rlu-files})
  refer to identifiers that are not declared in \textit{dirs/dir/unitname.fdl}.
  An alternative option is \texttt{-expect-dir-user-rules-with-undeclared-ids}.

  \optionb{read-directory-rlu-files}
  For each program unit with full name \textit{dirs/dir/unitname},
  read in the user-defined rules file \textit{dirs/dir/dir.rlu}.  The SPARK
  Simplifier reads in such rules files by default.

  \optionb{read-unit-rlu-files}
  For each program unit with full name \textit{dirs/dir/unitname},
  read in the user-defined rules file \textit{dirs/dir/unitname.rlu}.  
  The SPARK Simplifier reads in such rules files by default.

  \optionv{rules}{rulesfile} For every program unit, read in
    auxiliary rules file named in \textit{rulesfile}.  Multiple files
    can be specified using multiple \texttt{-rules} options.

  \optionb{expect-dir-user-rules-with-undeclared-ids}
  Directory-level user-defined rules files can sometimes include rules
  that involve type, function and constant identifiers that are not
  declared in the \fdl{} file for a unit being processed.  Normally, when
  Victor encounters a rule that has some undeclared identifiers, it
  deletes that rule and outputs a warning message to the log file.
  With this option, an info message rather than a warning message is
  output for directory-level user rules involving undeclared ids.  An
  alternative option is \texttt{read-all-decl-files-in-dir}.

  \optionb{siv} Read in \texttt{.siv} simplified VC files output by the
     Simplifier rather than \texttt{.vcg} Examiner VC files.

% See smt-driver.cc
\optionv{goal}{g} Only consider goal number $g$.
  %  Skipped over goals are not reported in \goalreportfile{} output file.  
  %
  This option is intended for use when Victor is run on a single unit,
  when a \textit{unit-name} argument and no \texttt{units} option is
  given.

\optionv{concl}{c} Only consider conclusions (goal slices) numbered $c$.  
  This option is intended for use when Victor is run on a single unit.

\optionb{skip-concls}
  Do not pass conclusion formulae to the selected prover.  This option is
  good for helping to identify goals or goal slices true because of an
  inconsistency in the hypotheses or rules.

\optionb{skip-hyps}
  Do not pass hypothesis formulae to the selected prover.  This option is
  good for helping to identify goals or goal slices true because of an
  inconsistency in the rules.

\optionv{skip-rule}{r} Do not pass rules with name matching pattern $r$ to
  the selected prover. The pattern $r$ can contain wildcards
  \begin{itemize}
  \item `\ttstar{}' matching 0 or more characters in the name, and
  \item `\ttqmark{}' matching exactly one character in the name.
  \end{itemize}

  The simple matching algorithm requires that any instance of
  `\ttstar{}' in $r$ be at the end of $r$ or be followed by some
  character other than `\ttstar{}' or `\ttqmark'.  If `\ttstar' is
  followed by some character \emph{c}, then the sequence of characters
  matched by `\ttstar' will not contain \emph{c}.

\optionb{skip-check} 
  Skip issuing command to prover to run a check of the asserted goal.
  This has been found helpful when debugging problems with the selected
  prover.

% See utility.cc
\optionv{from-unit}{unit-name}
  Only drive to selected prover the units listed in the \texttt{-units} option
  starting with \textit{unit-name}.  Default is to start with first. 

\optionv{from-goal}{g}
  In first unit to be passed to prover, start driving goals / goal
  slices to prover at goal $g$.

\optionv{to-unit}{unit-name}
  Stop driving units to the selected prover after \textit{unit-name} is 
  encountered. Default is to continue until the last listed unit.

\optionb{skip-units-with-no-rlu-files} 
   Run only on units with \rlu{} files.   This is particularly
   useful when doing user rule analysis.   
    See Section~\ref{sec:user-rule-analysis} below.



\optionv{active-unit-tags}{tags}
  Identify which tagged options (if any) in the unit listing file to make
  active.  See Section \ref{sec:unit-listing-file} for more on this.
  %
  Multiple tags should be separated by colons (\texttt{:}).

\optionb{include-selected-goals}
  When particular goals or goal slices are selected for a unit in the
  unit listing file, run Victor on just those goals or goal slices.

\optionb{exclude-selected-goals}
  When particular goals or goal slices are selected for a unit in the
  unit listing file, do not run Victor on those goals or goal slices.

\end{description}


%----------------------------------------------------------------------------
\subsection{Normalisation options}
%----------------------------------------------------------------------------
\emph{Normalisation} is the process of putting an \fdl{} unit into a
standard form where all ambiguities have been resolved.
Specifically, normalisation
\begin{itemize}
\item resolves the types of overloaded operators:
  \begin{itemize}
  \item \verb_+_, \verb_-_ (binary), \verb_-_ (unary), \verb_*_ on
    integer and real types,
  \item \verb_=_ and \verb_<>_ on any type,
  \item \verb_<_ , \verb_<=_, \verb_>_ and \verb_>=_ in integer, real and enumeration types,
  \item \verb_succ_ and \verb_pred_ on integer and enumeration types,
  \item array element update and element select functions, 
  \item record field update and field select functions,
  \end{itemize}

\item adds universal quantifiers to rules to bind and type any free
  variables in the rules.
\end{itemize}

After normalisation but before any translation steps are applied,
Victor does a full type check of the unit to ensure the integrity of
the unit.  If normalisation has not been completely successful, type
check error messages identify the issues.

Overload resolution is driven by the inferred types of each overloaded
operator's arguments.  So long as the argument types can indeed be
inferred, overload resolution is straightforward.  However, when an
argument is a free variable in a rule, sometimes Victor has difficulty
inferring which operator is intended, in which case overload
resolution fails.

Victor infers the type of a free variable by examining the typing of
the operator applied to each instance of the variable.  This works
fine if the operator is not overloaded. 

In the first phase of ambiguity resolution, Victor repeatedly
interleaves 
\begin{itemize}
\item attempts at operator overload resolution, and
\item inference of constraints on types of free variables 
\end{itemize}
until no further progress can
be made.  This phase is always sound.  In this phase Victor will never
speculatively resolve overloading or speculatively choose some type
for a free variable.

As mentioned above, if the ambiguity resolution has not been completed,
the subsequent type check will identify the issues.  To date, all the
observed issues have had at their root the failure to infer types of
free variables in user rules provided in \rlu{} files.  Invariably
the problem is with free variables which only appear as arguments to
overloaded operators.  To fix the issues, add extra explicit typing
assumptions of form \texttt{goal(checktype(\emph{var}, \emph{type}))}
to the rules identified in the error messages.  Usually the Simplifier
tool handles these typing assumptions properly.  However the
recommended practice is that it always be re-run after these
assumptions have been added in order to double check them.

This addition of explicit typing assumptions can require a fair amount
of work, especially if there are 100s of user rules and the \fdl{}
involves reasoning with operators over the reals.  For example, Victor
will observe that every free variable that could be typed
\texttt{real} could also be typed \texttt{integer}, and will therefore
refuse to assign the variable a type in this first phase.

By default ambiguity resolution stops at the first phase.  However,
Victor has three options which allow the user to tell Victor to go
onto a second phase of ambiguity resolution where extra assumptions
are made.  The options are:
\begin{description}
  \optionb{assume-var-in-real-pos-is-real} If a free variable occurs
  as an argument to an operator in a position where a real is
  expected, assume the variable has real type.
%
  \optionb{assume-int-or-real-var-is-real} If a free variable is
  constrained to have either integer or real type, assume the variable
  has real type.  This option subsumes the previous option.
%
  \optionb{assume-int-or-real-var-is-int} If a free variable is
  constrained to have either integer or real type, assume the variable
  has integer type.
\end{description}
%
At most one of these 3 options should be selected.  The first two
options are potentially unsound.  To avoid unsoundness when either of
these options is used, any free variable that ought to be integer must
be explicitly typed by a \texttt{checktype} precondition.  The third
option is always sound, but could result in rules that are overly
restrictive and not usable as expected by the Simplifier.  One
situation where the 3rd option might be appropriate is when \spark{}
programs being analysed involve no floating-point computations, and
hence when the generated VCs involve no terms of real type.

When any of these options is selected, Victor by default will insert a
warning message into the \logfile{} log file for each assumption it
makes, so each application of the assumption can be checked.  If these
warning messages are not needed, use the following option.
\begin{description}
  \optionb{suppress-warnings-of-var-type-assumptions} Suppress
  warnings of each application of an assumption about how a free
  variable should be typed.
\end{description}

%----------------------------------------------------------------------------
\subsection{Translation options}
%----------------------------------------------------------------------------

See Section \ref{sec:translation} for a presentation of these options,
since they make best sense in a discussion of the overall translation
process.

%----------------------------------------------------------------------------
\subsection{User rule analysis}
%----------------------------------------------------------------------------
\label{sec:user-rule-analysis}

These options analyse the rules that users add to the directory-level
and unit-level .rlu user rule files.  Users add rules to overcome
incompletenesses in the Simplifier prover and to provide extra
information that cannot easily be routed through the Examiner.  These
options help identify those rules required by the Simplifier, but not
some SMT solver.  They also help to pick out rules that inadvertently
are inconsistent.


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\subsubsection{Finding redundant rules}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

\begin{description}
  \optionb{find-redundant-rules} Consider each goal that is provable
  with all the user rules, and determine a minimal set of user rules
  needed to prove the goal.
    \begin{itemize}
    \item Report on which unit-level user rules are not in any of the
      minimal sets of the goals for a given unit.
      These unit-level user rules are redundant.
    \item Across all the goals in the units in a given directory, report 
      on which directory-level user rules are
      are not in any of the minimal sets for each goal in each unit.
    \end{itemize}
    The minimal set for a goal is found in a greedy fashion, starting
    with the full set of user rules, and then seeing if each rule in
    turn can be knocked out without affecting the provability of the
    goal.
    %
    The minimal set is similar to a proof summary / unsat core 
     see the documentation on the \texttt{-smtlib2-unsat-cores} option in 
    Section \ref{sec:prover-driving-options}).
    However, an unsat core might well include a user rule in a core because
    the SMT solver happened to first discover a proof using the rule, even if
    there are proofs without the rule.
    Here, when a user rule is considered, it is retained only if it is seen
    to be definitely needed.

\optionb{report-user-rule-status}
% was report-excluded-rlu-rules-per-goal
  For each goal, report the .vlg log file on the status of each user
  rule, whether it was
  \begin{enumerate}
  \item excluded from consideration because of unbound function,
    constant or type identifiers,
  \item considered and found to be outside the minimal set for that goal,
  \item considered and found to be inside the minimal set.
  \end{enumerate}

  
\end{description}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\subsubsection{Auditing rules}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

In a \emph{rule audit}, for each unit Victor completely discards the
goals read in from .vcg or .siv files and instead generates a set of goals
that check various properties of the user rules.  
%
The newly generated goals are divided into 5 kinds, as shown in
Table~{\ref{tab:audit-goal-kinds}}.
\begin{table}[htb]
  \newcommand{\uiname}{$u_i$-name}
  \centering
  \begin{tabular}{ccp{6cm}>{\ttfamily\ \ }ll}
    Kind   &    Goal shape  &  Description  &  \multicolumn{2}{c}{.vct tag} \\
    \hline
    A      &  $R \vdash \bot$ 
                      &  Are system rules inconsistent?
                                      & \ttfamily no urules  \\
    B      &  $R, U \vdash \bot$
                      &  Are user rules inconsistent?
                                      & all urules  \\
    C      &  $R, u_i \vdash \bot$
                      &  Is user rule $u_i$ inconsistent?
                                      & urule as H     & \uiname \\
    D      &  $R, \vdash u_i$
                      &  Is user rule $u_i$ derivable with no use of
                         other user rules?
                                      & urule as C   & \uiname \\
    E      &  $R, U\setminus\{u_i\} \vdash u_i$
                      &  Is user rule $u_i$ derivable from 
                         other user rules?
                         & urule from rest   & \uiname\\
  \hline
  \end{tabular}
  \caption{Kinds of Rule Audit Goals}
  \label{tab:audit-goal-kinds}
\end{table}

$R$ is the set of system rules, either generated by the Examiner
and read in from an .rls file, read in by Victor from one of its
standard rules files (e.g. \texttt{prelude.rul}), or generated by
Victor as part of its translation, 
%
and $U = \{u_1, \ldots, u_n\}$ is the set of user rules read in from
directory-level and unit-level user rule files, excluding those directory-level
rules that are not well formed because they have unbound constant, function or type identifiers.
%
For each unit, 1 goal of each of kinds A and B is generated, and $n$
goals of each of kinds C,D and E are generated.
%
The two columns labelled \emph{.vct tag} show what is output to the
\emph{goal origins} fields in the goal-based .vct report file.

Victor writes the number of goals of each kind that found to be true
to the .vus unit summary file, the .vsm session summary file and in an
extra audit report at the end of the .vlg log file.

The options are as follows.
\begin{description}
\optionb{do-rule-audit} Generate audit goals and collect results 
  in report files.
\optionb{rule-audit-a}  Include goals of kind A in audit.
\optionb{rule-audit-b}  Include goals of kind B in audit.
\optionb{rule-audit-c}  Include goals of kind C in audit.
\optionb{rule-audit-d}  Include goals of kind D in audit.
\optionb{rule-audit-e}  Include goals of kind E in audit.
\optionv{rule-audit-rule}{rname} 
  Generate audit goals just for rule with name \emph{rname} rather than
  for all of $u_1, \ldots, u_n$.  This option makes sense when attention
  is focussed on one unit or, if a directory-level rule is named, all
  units in a single directory.
\end{description}

%----------------------------------------------------------------------------
\subsection{Prover and prover interface selection}
%----------------------------------------------------------------------------

\begin{description}
\optionv{prover}{prover}
  Select the prover to drive.  Valid values of \emph{prover} are:
  \begin{itemize}
  \item \texttt{cvc3}
  \item \texttt{simplify}
  \item \texttt{yices}
  \item \texttt{z3}
  \end{itemize}
  A value of \texttt{none} can also be specified.  This is useful if
  one just wants to generate prover input files.

\optionv{prover-command}{prover-command}
  Use instead of the \texttt{prover} option to specify explicitly a
  shell-level command for invoking the prover.  This allows alternate
  provers or custom prover options to be specified.

  Selecting neither this option or the \texttt{prover} option is
  equivalent to setting the value of \texttt{prover} to \texttt{none}.
  
\optionv{interface-mode}{mode}
  Select the prover interface mode.  Valid values of \emph{mode} are:
  \begin{itemize}
  \item \texttt{api}: Use prover API.  
    Acceptable with \texttt{cvc3} or \texttt{yices}
    value for \texttt{prover}.

  \item \texttt{smtlib}: Use \smtlib{} 1.2 format files and
     stand-alone prover executable.
    Acceptable with \texttt{cvc3}, \texttt{yices} or \texttt{z3}
    value for \texttt{prover},
    and with \texttt{prover-command} option.

  \item \texttt{smtlib2}: Use \smtlib{} 2.0 format files and
     stand-alone prover executable.
    Acceptable with \texttt{cvc3} or \texttt{z3}
    value for \texttt{prover},
    and with \texttt{prover-command} option.

  \item \texttt{simplify}: Use Simplify-format files and
     stand-alone prover executable. 
    Acceptable with \texttt{simplify} or \texttt{z3} value for
    \texttt{prover}, 
    and with \texttt{prover-command} option.

%   \item \texttt{alt-simplify}: Use alternate Simplify-format files and
%      stand-alone prover executable. 
%     Acceptable with \texttt{simplify} or \texttt{z3} value for
%     \texttt{prover}, 
%     and with \texttt{prover-command} option.
%     These alternate Simplify-format files are generated by a customisation
%     of the code generating \smtlib{} interface.
  \item \texttt{dummy}: 
    Use some default code that mostly does nothing.  In this case,
    Victor still parses the VC files, does a prover independent
    translation of the goals, and generates \goalreportfile{}, \unitsumfile{},
    \sessionsumfile{} and \logfile{} output files.  This is the default option. 
  \end{itemize}

\end{description}

% \begingroup
% \newcommand{\tick}{$\bullet$}
% \begin{tabular}{l|ccccc}
%   Mode     &   \multicolumn{5}{c}{Prover}   \\
%            &  cvc3    & simplify   & yices & z3   & \textit{\rmfamily custom}\\
%   \hline

%   api      &  \tick   &            & \tick &      &          \\

%   simplify &          & \tick      &       &\tick & \tick         \\
%   smtlib   &  \tick   &            & \tick &\tick & \tick

  
% \end{tabular}
% \endgroup


%----------------------------------------------------------------------------
\subsection{Prover driving options}
%----------------------------------------------------------------------------
\label{sec:prover-driving-options}

\begin{description}
\optionb{fuse-concls} 
  Pass one goal at a time to the selected prover.  By default Victor
  passes one goal slice at a time.

\optionv{working-dir}{working-dir} 
  Use \textit{working-dir} as root of directory tree of files used for prover
  input and output.   An argument of  `\texttt{.}' is acceptable to indicate
  the current directory.  Defaults to \texttt{/tmp}.  
%  Option is currently only relevant for Simplify and \zthree.

  Unless one of the next three options is used, the same file
  names are used for every every prover run and every Victor run.

\optionb{hier-working-files}
   Use distinct files for each prover invocation and arrange in a
   hierarchical tree under \emph{working-dir}.

\optionb{flat-working-files}
   Use distinct files for each prover invocation and arrange all as 
   members of \emph{working-dir}.


\optionb{unique-working-files}
  Within a given Victor run, use the same file names for each prover
  invocation, but, by including hostname and process
  number in file names, make the names unique to the Victor run.
  %
  This option is useful if one wants to have simultaneous Victor runs.

\optionb{delete-working-files}
  Delete the files used for prover input and output after
  each prover invocation.

\optionb{add-formula-descriptions} 
  Add comments in the prover input file describing the rule, hypothesis
  or conclusion that each asserted formula comes from.

\optionb{smtlib2-unsat-cores}
  Ask the prover to report an unsatisfiability core for each proven goal.
  An \emph{unsatisfiability core} or \emph{unsat core} names which of
  the rules, hypotheses and the conclusion of a goal were used in the
  proof of the goal.  An unsat core can be viewed as a proof summary.
  Unsat cores are reported in the remarks field of records written to the
  \goalreportfile{} file.

  Unsat cores are currently only supported if the \smtlib{}2 file-level
  prover interface is used.

  Generation of unsat cores can slow down provers.  For example,
  \zthree's run-time on provable goals has been observed more than
  double when unsat core generation has been requested.

\optionb{smtlib2-add-to\_real-decl}
  Add a declaration for the \smtlib{} 2 \verb+to_real+ operator.  This is needed
  for \altergo{}.

\optionb{smtlib2-implicit-to\_real}
  Remove all occurrences of the \smtlib{} 2 \verb+to_real+ operator in
  \smtlib{} 2 format files created by Victor.  The \smtlib{} 2 standard
  allows these operators to be implicit.  This option is needed for
  supporting \cvcfour{} 1.0.

\optionv{ulimit-timeout}{time}
  If using either of the file-level interface modes, 
   use the Linux 
  \emph{ulimit} process limit facility to time out
  prover invocations after \emph{time} seconds.  The \texttt{time} value 
  should be a natural number.
  The default is not to time out prover invocations.

\optionv{watchdog-timeout}{time}
  %
  If using the \smtlib{}2 file-level interface mode, use the provided
  \emph{watchdogrun} C program to time out prover invocations after
  \emph{time} seconds of inactivity on the prover's output.  The
  \texttt{time} value can be a natural number or a fixed-point
  number (e.g. 0.1).  The default is not to time out prover invocations.

  The timeout measurement from the last output activity (or prover
  start time) is useful when a single call of the prover is used to
  answer multiple queries.  When timeouts are measured this way, they
  bound the run-time of the prover on the current query it is
  attempting, rather than also including in the allowed run period the
  times spent by the prover answering previous queries in a query set.

\optionv{smtlib2-soft-timeout}{time}
 %  
 If using the \smtlib{}2 file-level interface mode and \zthree{} v3.1 or newer,
 timeout \emph{check-sat} prover invocations after \emph{time} milliseconds.
 The \texttt{time} value should be a natural number.

\optionv{shell-timeout}{time}
  If using either of the file-level interface modes, 
   use the provided shell script 
   \texttt{timeout.sh} to time out prover invocations after \emph{time} 
  seconds.  The \texttt{time} value can
  be a natural number or a fixed-point number (e.g. 0.1).
  The default is not to time out prover invocations.

  Currently this option is not that robust and use of \texttt{-ulimit-timeout}
  is recommended instead.

\optionv{logic}{logic}
  If using the \smtlib{} interface mode, set the value of the 
  \texttt{:logic} attribute in the \smtlib{}-format files to \emph{logic}.
  The default is \texttt{AUFLIA}.

\optionb{smtlib-hyps-as-assums}
  If using the \smtlib{} interface mode, insert each hypothesis into
  the \smtlib{}-format file as the value of a distinct 
  \texttt{:assumption} attribute.
  
\optionb{use-alt-solver-driver}
  This option enables an alternative driver.  The new
  major features supported by this driver are \emph{incrementality} (see
  next option) and \emph{user rule analysis} (see
  Section~\ref{sec:user-rule-analysis}).
  
\optionb{exploit-solver-incrementality}
  This option gives significant reductions in prover run-time.

  Prior to summer 2011, the main solver driver always handed goals
  to the solver one at a time.  Each solver invocation had a complete
  separate copy of all the declarations and rules, even though these
  are constant across the goals of a unit. 

  With this option, when driving a unit, declarations and rules are
  passed to the solver just once, rather than repeatedly for each
  goal.  Use is made of solver support for pushing and popping
  contexts.

  This option has been tested with the \smtlib{} 2 file-level
  interface.  It ought to work with both the \yices{} and \cvcthree{}
  API interfaces, though this has not yet been fully enabled.

  When using the file-level \smtlib{} 2 interface, the driver
  initially creates a single \smtlib{} 2 format file containing
  queries for all the goals in a unit.  If the solver is killed
  because it timed out on some goal, a new solver input file is
  created just for the remaining goals. On each further timeout, a
  further new solver input file is created.

  This option is best used in conjunction with
  \texttt{-watchdog-timeout} or \texttt{smtlib2-soft-timeout} to
  ensure timeouts are applied to each individual query.  The
  \texttt{smtlib2-soft-timeout} option gives better performance, as
  the solver is then not killed on timeouts, and after a timeout can
  continue on further goals from the same input file: there is no need
  for rerunning the solver on a new file containing the remaining
  goals. However, for some reason, when run with the same time limits,
  the coverage with the soft timeout is lower.  This is currently being
  investigated.
  


% % smt-driver.cc
% \optionv{drive-goal-repeats}{count}
%    Repeat each prover invocation \textit{count} times.
%    This is used to increase precision of prover runtime measurements when
%    using an API interface.

% \optionv{check-goal-repeats}{count}
%    Repeat each prover invocation \textit{count} times.
%    This is used to increase precision of prover runtime measurements when
%    using a file-level interface.  

\end{description}

%----------------------------------------------------------------------------
\subsection{Output options}
%----------------------------------------------------------------------------


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\subsubsection{Screen output options}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

\begin{description}
\optionb{utick} Print to standard output a \texttt{*} character at the 
  start of processing each unit.
  If \texttt{-longtick} also selected, print instead 
  the unit name.
\optionb{gtick} Print to standard output a \texttt{;} character at the 
  start of processing each goal.  
  If \texttt{-longtick} also selected, print instead 
  the goal number.
\optionb{ctick} Print to standard output a \texttt{.} character at the 
  start of processing each conclusion of a goal.
  If \texttt{-longtick} also selected, print also
  the conclusion number.
\optionb{longtick} See above.

\optionb{echo-final-stats}
  Print to standard output the final statistics that are included at the
  end of the report file.
\end{description}


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\subsubsection{General report file options}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

\begin{description}
\optionv{report}{report-file}

  Use \textit{report-file} as body of filenames for \goalreportfile{},
  \unitsumfile{}, \sessionsumfile{} and \logfile{} report files.  Default
  is to use \texttt{report}.

\optionv{report-dir}{dir}
   Put report files in directory \textit{dir}.  If directory does not exist,
   it is created.  Default is to use current directory.
\end{description}

%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\subsubsection{VCT file options}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 


\begin{description}

\optionb{count-trivial-goals}

   Write an entry to the \goalreportfile{} file for each \spark{} input goal 
   of form \texttt{*** true}.
   In VCG files, these are the goals proven by the Examiner.
   In SIV files, these are the goals proven by the Examiner or the 
   Simplifier.
   These entries have the status \texttt{trivial} recorded in the status field.

   Use this option along with option \texttt{-fuse-concls} to have the
   goal counts match those from the POGS (Proof Obligation Summariser)
   tool.

\optionb{hkinds} Report list of hypothesis kinds \goalreportfile{} file records.
\optionb{ckinds} Report list of concl kinds in \goalreportfile{} file records.
\optionb{gstime} 
  Report time taken by prover to process a goal 
       in time field of \goalreportfile{} file records.
\optionb{gstime-inc-setup}
  Include setup time in gstime.  This setup time is time to 
  send declarations, rules, hypotheses and conclusions to the prover before
  invoking prover itself.  

  It is appropriate to include this time when calling the prover via 
  an API (\yices and \cvcthree{} cases) since
  the provers do incremental processing on receiving this information.
  When the prover interface is via files, this setup time is the time to 
  write an input file for the prover, so it is not as appropriate to include
  it.

\optionb{csv-reports-include-goal-origins}
  Include information on goal origins in goal origins fields of 
  \goalreportfile{} file records.
  Default is not to include this information.

\optionb{csv-reports-include-unit-kind}
  Include information on unit kind in unit kind field of \goalreportfile{} file
  records.  For example, whether the unit is a function or a procedure.
  Default is not to include this information.
\end{description}

%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\subsubsection{Log file options}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

\begin{description}
  \optionv{level}{level}  Report all messages at or above 
     priority \textit{level}.  The levels and associated names are
     \begin{enumerate}
     \item [6] \texttt{error}
     \item [5] \texttt{warning}
     \item [4] \texttt{info}
     \item [3] \texttt{fine}
     \item [2] \texttt{finer}
     \item [1] \texttt{finest}
     \end{enumerate}
     The \textit{level} value can either be a number or the associated name.
     The default level is \emph{warning}.

\end{description}

%----------------------------------------------------------------------------
\subsection{Debugging options}
%----------------------------------------------------------------------------
\begin{description}
\optionb{scantrace} Write lexer debugging information to standard output 
\optionb{parsetrace} 
  Write parser debugging information to standard output 
\end{description}

%----------------------------------------------------------------------------
\subsection{CVC3 options}
%----------------------------------------------------------------------------

Unless otherwise specified, these options are only relevant when invoking
\cvcthree{} via its API.
%
The main options are as follows.
\begin{description}
\optionb{counterex}
   Report counterexamples for false and unknown queries. 

\begin{remark}
I have not figured out yet how to direct \cvcthree{} to write counter-examples
to files.   A work-around to view counter-examples is to run with 
this option and the \texttt{-cvc-inputlog} option, and then run the
standalone \cvcthree{} executable on the generated \cvcthree{} input file.
\end{remark}

% \optionv{resourcelimit}{limit}
%   Set resource limit for \cvcthree{} runs.  This provides a soft timeout
%   option.
%   A value of 25,000 gives run time limits of 7-10sec on a 1.86GHz Intel
%   Core 2 processor.  Default is 0, no limit.

%   This option also works when invoking \cvcthree{} on \smtlib{}-format input
%   files.

\optionv{timeout}{time}
  Set a timeout period in units of 0.1 seconds for runs of \cvcthree{}, both
  via API and via executable.  Uses \cvcthree{}'s internal support for
  timing out.
  
\optionb{cvc-loginput}
  Enable echoing of API calls for each \cvcthree{} run to a file. 
  Use the \texttt{-working-dir} option to set where the file is stored
  and the 
  \texttt{-hier-working-files} and \texttt{-flat-working-files} options
  to control whether and how distinct files are used for each run. 
  %
  Files have suffix \texttt{.cvc}.
  %
  If distinct files are not requested,
  all runs will be echoed to a file named \texttt{cvc3.cvc},
  each run overwriting the previous one.
  %
  These files are saved in \cvcthree{}'s standard input language and can be 
  used as input to a \cvcthree{} stand-alone executable.

% \optionv{cvc-echo-suffix}{suffix}
%   Set suffix to use for file logging \cvcthree{} calls.  Defaults to 
%   \texttt{.clog}.
\end{description}
See the file \texttt{cvc-driver.cc} for further available options.  Not
all of these have been tried out yet.


%----------------------------------------------------------------------------
\subsection{Simplify options}
%----------------------------------------------------------------------------

No options are currently available.

%----------------------------------------------------------------------------
\subsection{Yices options}
%----------------------------------------------------------------------------

Unless otherwise specified, these options are only relevant when invoking
\yices{} via its API.

\begin{description}
\optionb{yices-loginput}
  Enable echoing of API calls for each \yices{} run to a file. 
  Use the \texttt{-working-dir} option to set where the file is stored
  and the 
  \texttt{-hier-working-files} and \texttt{-flat-working-files} options
  to control whether and how distinct files are used for each run. 
  %
  Files always have suffix \texttt{.yices}.  If distinct files are not
  requested, all runs will be echoed to the file 
  \texttt{yices.yices}, each run overwriting the previous one.
  %
  These files are saved in \yices{}'s standard input language and can be 
  used as input to a \yices{} stand-alone executable.
\begin{remark}
%   The \yices{} executable preloads declarations of functions \texttt{div}
%   and \texttt{mod}.  The \yices{} input files output by Victor might
%   need editing to remove declarations of these functions before the input
%   files will execute properly. 
  %
  Victor lets \yices{} reject non-linear parts of formulae - see the
  warnings in Victor's log file.  These formulae might have to be removed by 
  hand for \yices{} to load these input files properly.
\end{remark}


\optionb{yices-logoutput}
  Set file for output of each run of \yices{}. 
  Location of file and whether distinct files generated for each run
  are specified in same way as with \texttt{-yices-loginput}.
  Suffix of files is \texttt{.ylog}.  If distinct files not requested,
  all runs written to \texttt{yices.ylog}.

% \optionv{yverb}{n} 
%   Set verbosity of \yices's output to \textit{n}.

\optionb{counterex} 
   Enable reporting of counter-example models to output log file.

% -ynotc          Disable Yices type checking (enabled by default).

% -abstract-nonlin-divmod
%                 Abstract nonlinear divmod exps to uninterpreted functions.
%                 Default is to abstract all divmod exps.
% -abstract-nonlin-times
%                 Abstract nonlinear times exps to uninterpreted functions.
%                 Default is to abstract no times exps.

\optionv{timeout}{time}
  Set a timeout period in seconds for runs of the \yices{} executable 
  on \smtlib{}-format input files.   Uses \yices{}'s \texttt{--timeout}
  option.

\end{description}
%\fixme{Do anything about non-linear arithmetic options?}


%----------------------------------------------------------------------------
\subsection{Z3 options}
%----------------------------------------------------------------------------

No \zthree{} options are specifically supported by Victor.  \zthree{} options
can be specified by giving a custom prover command with the \texttt{prover-command} option.

% \begin{description}
% \optionb{z3-fourier-motzkin}
%   Use Fourier-Motzkin elimination to eliminate all quantifiers over linear
%   arithmetic expressions.
% \end{description}



%============================================================================
\section{Translation}
%============================================================================
\label{sec:translation}

% As defined in (p:) processor.cc and (t:) translation.cc

The description of the translation
process here is rather brief and not self-contained.
%
The process is best understood by first having a read of the
draft paper \emph{Proving SPARK Verification Conditions with SMT solvers},
available from the author's website.

Unless otherwise stated, translation steps are carried out in order
they are described in below.

%----------------------------------------------------------------------------
\subsection{Standard Form translation}
%----------------------------------------------------------------------------

Most translation steps in Victor are carried out on units in a standard form.
In this standard form all functions and relations have a unique type, 
there is no overloading.

The first translation step is to put units into this standard form.

% p;putUnitInStandardForm

\begin{itemize}
% p:augmentConstDecls

\item Some constants with names of form 
   $\mathit{c}\mathtt{\_base\_first}$
   or $\mathit{c}\mathtt{\_base\_last}$
   are used but not declared.  Victor adds declarations for such constants
   when they appear to be missing, when e.g. the constant
   $\mathit{c}\mathtt{\_first}$ is declared ($c$ not with suffix $\mathtt{\_base}$) and the constant 
   $\mathit{c}\mathtt{\_base\_first}$ is not declared.

\item The \fdl{} files output by the Examiner are missing declarations
  of the $\mathit{E}\_\_\mathtt{pos}$
  and $\mathit{E}\_\_\mathtt{val}$ functions used by each enumeration type
  $E$, including the implicitly declared \texttt{character} type.  These
  declarations are added in.

\item \fdl{} variables are considered as semantically the same as
  \fdl{} constants.  Each declaration of an \fdl{} variable $x$, is
  changed to a constant declaration, and new declarations are added
  for names \textit{x}\tttilde{} and \textit{x}\texttt{\%}.  \fdl{}
  units use the names \textit{x}\tttilde{} and \textit{x}\texttt{\%}
  to refer to the value of $x$ at procedure and loop starts
  respectively.


\item Occurrences of the \fdl{} operator \texttt{sqr(x)} are replaced by 
  \texttt{x ** 2}.

\item Distinct operators are introduced for the standard arithmetic operations
  $+$, $\times$, $-$(unary), $-$(binary) over the integers and reals,
  and an explicit coercion operator is introduced for converting integers
  to reals.

\item Distinct relations are introduced for the inequality relations 
  over integers, reals, and enumeration types. 

\item Distinct versions of the \fdl{} operator \texttt{abs(x)} are introduced
  for the real and integer types.   Defining axioms are added to the set
  of rules for each unit.

\item A defining axiom is added for the \fdl{} predicate \texttt{odd(x)}.

\item Some characterising axioms are added for the \fdl{} operator
   \texttt{bit\_\_or(x)}.  No axioms are added yet for other bit-wise
   arithmetic operators.

\item The \fdl{} language overloads the functions \texttt{succ} and
  \texttt{pred} and inequality relations such as $<$ and $\leq$.
  %
  Distinct versions are introduced for the \fdl{} \texttt{integer} type
  and each enumeration type and declarations are added for each of
  these versions.

\item The Examiner outputs rules with implicitly quantified variables.
  Victor infers the types of these variables and makes the
  quantifications explicit.  The explicit quantification is needed by
  all the provers to which Victor interfaces.

\end{itemize}


%----------------------------------------------------------------------------
\subsection{Type checking}
%----------------------------------------------------------------------------

Victor type checks units after translation into standard form
and after all translation steps have been applied.


%----------------------------------------------------------------------------
\subsection{Enumerated type abstraction}
%----------------------------------------------------------------------------

\begin{description}
\optionb{abstract-enums} 
  Replace enumerated types with abstract types, introduce all
  enumeration constants as normal constants, and keep all enumerated
  type axioms.  
  %
  These axioms are introduced by the Examiner to
  characterise enumerated-type-related functions such as
  $\mathit{E}\mathtt{\_\_val}$ and $\mathit{E}\mathtt{\_\_pos}$ and
  can serve as a partial axiomatisation of the introduced
  abstract types.

\optionb{elim-enums}      
  Replace each enumeration type $E$ with an integer subrange type $\{0
  \ldots k - 1 \}$ where $k$ is the number of enumeration constants in
  $E$.
  % 
  Declare each enumeration constant as a normal constant, and add an axiom
  giving its integer value.
  %
  Delete all existing enumerated type axioms and add in new axioms
  characterising enumerated-type-related functions such as 
  $\mathit{E}\mathtt{\_\_val}$ and  $\mathit{E}\mathtt{\_\_pos}$.

\optionb{axiomatise-enums}
  Replace each enumeration type $E$ with an uninterpreted type, and add
  axioms characterising the the uninterpreted type as isomorphic to the
  integer subrange $\{0 \ldots k - 1 \}$ where $k$ is the number of
  enumeration constants in $E$.
  %
  The added axioms replace the enumerated-type-related axioms
  introduced by the Examiner and provide a full axiomatisation of
  the enumerated types.

\end{description}

%----------------------------------------------------------------------------
\subsection{Early array and record abstraction}
%----------------------------------------------------------------------------

\begin{description}
\optionb{abstract-arrays-records-early} Enable abstraction at this point
\end{description}
See Section~\ref{sec:late-arr-rec-abs} below for rest of options

%----------------------------------------------------------------------------
\subsection{Separation of formulas and terms}
%----------------------------------------------------------------------------

In \fdl{} formulas are just terms of type Boolean.   Many provers require
the traditional first-order logic distinction between formulas and terms.
%
The options here control the introduction of this distinction.

Victor calls the term-level Booleans \emph{bits}.


\begin{description}
\optionb{bit-type} Enable separation.  
\optionb{bool-eq-to-iff}
  Initially convert any equalities at Boolean type to `if and only if's.
  If an equality is at a formula position, then this results in the
  arguments to the equality changing from being at a term position to
  being at a formula position.  This is useful when the
  \texttt{-bit-type-with-ite} option is not asserted, and arguments
  involve operators (e.g. logical quantifiers) that can then only occur
  at formula positions.

\optionb{bit-type-with-ite} Whenever possible, introduce instances
  of the `if-then-else' operator rather than term-level versions of
  propositional logic operators and atomic relations.  This is
  particularly useful when logical operators (e.g. quantifiers) occur
  in term positions.
  
\optionb{bit-type-prefer-bit-vals}
  A heuristic for controlling whether atomic relations are translated
  to term-level (bit-valued) functions or first-order-logic formula-valued
  relations.
  %
  With this heuristic, bit-valued functions are preferred.

\optionb{bit-type-prefer-props}
  Another heuristic for controlling whether atomic relations are translated
  to term-level (bit-valued) functions or first-order-logic formula-valued
  relations.
  With this heuristic, formula (propositional) relations are preferred.

  If neither this option or \texttt{-bit-type-prefer-bit-vals} is selected,
  the default behaviour is to use a bit-valued function just when 
  there is one or more occurrences at the term level.

\optionb{trace-prop-to-bit-insertion}
  Report in log file when a proposition-to-bit coercion (encoded using the
  `if then else' operator) is added.
 
\optionb{trace-intro-bit-ops-and-rels}
  Report in log file when term-level function is introduced for a function
  (either user-defined or built-in) that initially had Boolean value type.

\end{description}

NB: the \spark{} \fdl{} language has `bit' operators 
\texttt{bit\_\_or},
\texttt{bit\_\_and} and 
\texttt{bit\_\_xor}.
%
These \fdl{} operators take integers as arguments and return integers
as results.  Their result values correspond to the correct unsigned
binary result for the respective operations on unsigned binary
versions of the arguments.  Axioms on these operators capture the
arithmetic properties of Boolean operations on finite-length binary
words.
%
If the Victor option \texttt{-abstract-bit-ops} is used, Victor introduces 
operators
\texttt{bit\_\_\_or},
\texttt{bit\_\_\_and} and 
\texttt{bit\_\_\_xor}. (Note the 3 `\texttt{\_}' characters rather than 2.)
%
These operators work on the term-level Booleans introduced by Victor and
are distinct from the \spark{} \fdl{} bit operators.

%----------------------------------------------------------------------------
\subsection{Type refinement}
%----------------------------------------------------------------------------

\begin{description}
\optionb{refine-types} Master control

\optionb{refine-bit-eq-equiv} 
  Add in definition for bit-valued non-trivial equivalence relations.
  Needed when \\ \texttt{-bit-type-with-ite} option not previously selected.

\optionb{refine-int-subrange-type}       
\optionb{refine-bit-type-as-int-subtype}
\optionb{refine-bit-type-as-int-quotient}
\optionb{refine-array-types-with-quotient}

\optionb{refine-array-types-with-weak-extension-constraint}
  Constrain values of element and extended indices using possibly non-trivial
  equivalence relation on element type.  Default is to use equality to
  constrain these values.

  Only applies if option \texttt{-refine-array-types-with-quotient} is not
  selected.

\optionb{refine-uninterpreted-types}
  Refine every uninterpreted type to be predicate subtype of a new 
  uninterpreted type.  Use this to ensure that exists model in which 
  every uninterpreted type can be interpreted by some infinite set.

\optionb{no-subtyping-axioms}
  Suppress generation of axioms for sub-typing properties of functions and
  constants.

\optionb{no-functionality-axioms}
  Suppress generation of axioms for functionality properties of functions and
  relations.

\optionb{strong-subtyping-axioms}
  Use subtyping axioms without constraints on values of arguments.

\optionb{trace-refine-types-quant-relativisation}
  Report in log file whenever a quantifier is relativised.

\optionb{trace-refine-types-eq-refinement}
  Report in log file whenever an equality relation is refined to a non-trivial
  equivalence relation.

\optionb{trace-refine-types-bit-eq-refinement}
  Report in log file whenever an term-level equality relation is refined to 
  a non-trivial term-level equivalence relation.
\end{description}

%----------------------------------------------------------------------------
\subsection{Late array and record abstraction}
%----------------------------------------------------------------------------
\label{sec:late-arr-rec-abs}

\begin{description}
\optionb{abstract-arrays-records-late}  Enable abstraction at this point
  in translation.  

% Eliminate redundant operators
%------------------------------
\optionb{elim-array-constructors}
  Eliminate all occurrences of array constructors
\optionb{elim-record-constructors}
  Eliminate all occurrences of record constructors
\optionb{abstract-record-updates}
  Introduce axiomatic characterisations for record update operators in 
  terms of record constructors and record field selectors.

% Add axioms defining types axiomatically
%-----------------------------------------

\optionb{add-array-select-update-axioms}
  Assumes that array constructors have first been eliminated.

\optionb{add-array-extensionality-axioms}

\optionb{add-record-select-constructor-axioms}
  Assumes that record update operators have first been eliminated.

\optionb{add-record-constructor-extensionality-axioms}
  Add extensionality axioms involving record constructors and field select
  operators.

\optionb{add-record-select-update-axioms}
  Assumes that record constructors have first been eliminated.

\optionb{add-record-eq-elements-extensionality-axioms}
  Add extensionality axioms stating that records are equal just when
  all fields are equal.
  
\optionb{use-array-eq-aliases}
  Introduce aliases for equalities at array types in order
  to help with matching extensionality  axioms.

\optionb{use-record-eq-aliases}
  Introduce aliases for equalities at record types in order
  to help with matching extensionality  axioms.

% Abstract operators and types
%------------------------------
\optionb{abstract-array-select-updates}
  Change primitive array element select and update operators into 
  uninterpreted functions.
\optionb{abstract-array-types}
  Replace array types with uninterpreted types.


\optionb{abstract-record-selects-constructors}
  Change primitive record field selectors and constructors 
  into uninterpreted functions.
\optionb{abstract-record-selects-updates}
  Change primitive record field selectors and field update operators
  into uninterpreted functions.

\optionb{abstract-record-types}
  Replace record types with uninterpreted types.
\end{description}



%----------------------------------------------------------------------------
\subsection{Bit abstraction}
%----------------------------------------------------------------------------

\begin{description}
\optionb{abstract-bit-ops}
  Replace primitive bit-type operators with uninterpreted functions 
  and add characterising axioms

\optionb{abstract-bit-valued-eqs}
  Replace primitive bit-valued equality operators with uninterpreted functions 
  and add characterising axioms

  \optionb{abstract-bit-valued-int-real-le} 
  Replace primitive
  bit-valued inequality operators on integers and reals with
  uninterpreted functions and add characterising axioms

\optionb{elim-bit-type-and-consts}
  Replace primitive bit type with either integer type or $\subrange{0}{1}$ 
  subrange type, depending on whether type has been refined earlier or not.
  Replace primitive bit-type constants for true and false with $0$ and $1$.

%\optionb{abstract-bit-type-and-consts}
% Not implemented
\end{description}


%----------------------------------------------------------------------------
\subsection{Arithmetic simplification}
%----------------------------------------------------------------------------

\begin{description}
\optionb{elim-consts}
  %
Eliminate integer and real constants. Rewrite all formulae using
hypotheses of form $x = k$ where $x$ is an \fdl{} constant or
variable, and $k$ is either a ground integer literal build from a
natural number and possibly unary minus or a ground real literal
involving one or more integer literal(s) and possibly unary minus and
real division.  This eliminates the apparent syntactic non-linearity
of some hypotheses and conclusions.

  It is particularly useful for Yices which rejects formulae that
  appear non-linear.


\optionb{ground-eval-exp}
  Evaluate occurrences of exponent function with natural number arguments.

\optionb{ground-eval}
  Evaluate ground integer arithmetic expressions involving $+$, $-$
  (unary and binary), $\times$, integer division, integer modulus, and
  the exponent function.

\optionb{expand-exp-const}
  Expand natural-number powers of integer and real expressions into products,
  with special-case treatment for exponents 0 and 1.

\optionb{add-ground-exp-eval-axioms}
  Add rule \[n \verb+**+ m = v\] where $n$,$m$ and $v$ are natural numbers and
  $v = n^m$ 
 if
 \begin{enumerate}
 \item $n \verb+**+ m$ with $n$,$m$ natural numbers is found in unit, or
  \item natural number $p$ is found in unit, where $p = 2^m$ or $p = 2^m -1$
    for some m in range $1 \ldots 64$.
  \end{enumerate}
  These rules help \smt{} solvers to instantiate rules from 
  Victor's rule prelude that provide upper bounds on values of the functions
  \texttt{bit\_\_or} and 
  \texttt{bit\_\_xor}, and involve use of the exponent function.

  If this option is used, do not use option \texttt{-ground-eval-exp} or 
  \texttt{-ground-eval}.

  This option modifies the behaviour of \texttt{-expand-exp-const} so 
  it does not expand terms of form $n \verb+**+ m$ when both $m$ and $n$ are
  natural numbers.

\optionv{exp-2-bound}{b}  When using option 
  \texttt{-add-ground-exp-eval-axioms}, set upper bound for $m$ to
  something else other than default of 64.


\optionb{arith-eval}
  Apply the rewrite rules
  \begin{eqnarray*}
   k \times (k' \times e)   & =  &  kk' \times e \\
   (k \times e) \times k'   & =  &  kk' \times e \\
   e \times k               & =  &  k \times e \\
   (k \times e) \times (k' \times e') &  =  &  kk' \times (e \times e') \\
   e \times (k \times e')   &  = &  k \times (e \times e')  \\
   (k \times e) \times e'   & =  &  k \times (e \times e')  \\
  (k \times e) \div k'      & =  &   (k \div k') \times e  
      \quad\mbox{if $k'$ divides $k$}.
  \end{eqnarray*}
  The main aim of these rules is to eliminate instances of the $\div$
  operator.

\optionb{push-down-to\_real}
  Rewrite applications of the integer-to-real conversion (\verb+to_real+
  in \smtlib 2) to integer arithmetic operators $\times, +, - (unary), -
  (binary)$, replacing the operators with their real counterparts and
  pushing the conversion down the term tree.  Also rewrite applications
  of the conversion to integer literals to corresponding real literals.

  
\optionb{sym-consts}
  Replace each distinct natural number literal greater than 
  threshold \textit{t} with a new constant and assert axioms concerning
  how these new constants are ordered: if the new constants in increasing
  order are $c_1 \ldots c_n$, the axioms are 
  $t < c_1, c_1 < c_2, \ldots, c_{n-1} < c_n$.

  This option is used to try to reduce the frequency of machine
  arithmetic overflow with Simplify.  Other users of Simplify try
  thresholds of 100,000, though we've observed overflows with
  thresholds as low as 1000.

\optionv{sym-prefix}{prefix}
  Set prefix for new symbolic number constants.  Default prefix is
  \texttt{k\_\_\_}.


\end{description}



%----------------------------------------------------------------------------
\subsection{Arithmetic abstraction}
%----------------------------------------------------------------------------
The different interfaces and provers vary in the classes of arithmetic
operations they can handle.  These options allow one to abstract to
uninterpreted functions, possibly adding some characterising axioms,
when operations cannot be handled.

\begin{description}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\optionb{abstract-nonlin-times}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  Abstract each integer and real multiplication unless at least
  one of the arguments is a fixed integer or real constant.

  An \emph{integer constant} is a natural number $n$ or the expression $-n$.
  
  A \emph{real constant} is built from an integer constant using the
  \texttt{to\_real} coercion, unary minus on the reals, and, optionally
  real division.  Real division is allowed just when the option 
  \texttt{-abstract-real-div} is not chosen.

  The \yices{} API usually rejects individual hypothesis or conclusion
  formulas if they have non-linear multiplications.  However, it does
  accept non-linear multiplications in quantified formulas, and
  will use linear instantiations of these formulas. 
  %
  Unfortunately, it currently aborts on finding a non-linear
  instantiation rather than simply rejecting the instantiation.

  The \smtlib{} sub-logics \textsc{auflia} and \textsc{auflira} both 
  require all multiplications to be linear.

%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\optionb{abstract-non-const-real-div}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 

  Abstract each real division unless the both argument are real constants.
  Needed by SMTLIB logics that support linear reals.


%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\optionb{abstract-exp}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  Replace occurrences of integer and real exponent operators by new 
  uninterpreted functions.  Currently no defining axioms are supplied, though
  it would be easy to do so. 

  This abstraction only happens after possibly evaluating ground 
  and constant exponent instances.

  Only the \cvcthree{}-via-API prover alternative can handle these
  operators directly.

%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\optionb{abstract-divmod}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  Replace occurrences of integer division and modulus operators by new 
  uninterpreted functions.  

%   There are two alternative rule sets provided
%   that can be loaded using the \texttt{-rules} option.
%   \begin{itemize}
%   \item \texttt{divmod.rul}: Exactly characterises \texttt{div} and gives
%     bounds on \texttt{mod} values.
%   \item \texttt{divmod-full.rul}
%     Exactly characterises both \texttt{div} and \texttt{mod}. 
%     These rules are probably more than is necessary in most cases. 
%     %
%     They have not been tried recently.  
%   \end{itemize}

%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\optionb{abstract-real-div}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  Abstract occurrences of real division to a new uninterpreted function.
  No characterising axioms are currently provided.

  \yices-API, \cvcthree-API and \zthree-\smtlib{} all allow input 
  with the real division operator, though it is not known what kinds of
  occurrences are accepted in each case.

  The official \smtlib{} logics involving reals do not allow real division.
  The assumption is that pre-processing has eliminated all occurrences of
  real division.  Victor doesn't yet carry out such pre-processing.

%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\optionb{abstract-reals}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  Abstract occurrences of real arithmetic operations 
  ($+$, unary $-$, binary $-$, $*$, $/$), integer to real coercions, and
  real inequalities to new uninterpreted functions.

  Currently this is needed by the \smtlib{} and Simplify translations.
  The \smtlib{} driver does not attempt to make use of the limited
  support in some of the \smtlib{} sub-logics for reals.

  This option is not necessary when \cvcthree{} and \yices{} are
  invoked via their APIs, as both APIs support real arithmetic.

%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
\optionb{abstract-to\_real}
%- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  %
  Abstract occurrences of the integer-to-real conversion operator to a
  new uninterpreted function.  No characterising axioms are currently
  provided.  

  This option is needed to support \altergo{} v0.95 and before, since
  these provers do not recognise this operator.
  


\end{description}




%----------------------------------------------------------------------------
\subsection{Final translation steps}
%----------------------------------------------------------------------------

\begin{description}
\optionb{elim-type-aliases}
  Normalise all occurrences of type identifiers in type,
  constant, function and relation declarations and in all formulas.
  %
  Normalisation eliminates all occurrences of type ids $T$ that have a
  definition $T \doteq T'$ where $T'$ is either a primitive atomic
  type (Boolean, integer, integer subrange, real or bit type) or is
  itself a type id.

  This is needed for the \smtlib{} and Simplify translations.

\optionb{switch-types-to-int}
  Replace all occurrences of type identifiers in 
  constant, function and relation declarations and in all formulas with
  the integer type. 
  % 
  Checks that every defined type is either an alias for another defined
  type or an alias for the integer type. 
  %
  This translation step assumes that a countably infinite model exists
  for every uninterpreted type. 

  This option is is needed for the Simplify translation.

  
\optionb{lift-quants}
  Apply the rewrite rule
  \[
      P \Implies \forall x:T.\ Q \quad\Iff\quad  \forall x:T.\ P \Implies Q
  \]
  ($x$ not free in $P$) 
  to all formulae.  The quantifier instantiation heuristics in both 
  \zthree{} and Simplify work better when universal quantifiers in 
  hypotheses are all outermost.

\optionb{strip-quantifier-patterns}

Some of the universally-quantified axioms introduced by translation
have trigger patterns giving hints on how instantiations can be guessed.
%
This option strips out these patterns.

\end{description}



%============================================================================
\section{CSV utilities}
%============================================================================
These utilities are very useful for analysing and comparing results of Victor
runs.

%----------------------------------------------------------------------------
\subsection{Filter CSV records}
%----------------------------------------------------------------------------
Usage:
\begin{quote}
   \texttt{csvfilt} [\texttt{-v}] \textit{n str} [\textit{file}]
\end{quote}
Filter \csv{} records, returning on standard output just those with
\textit{str} a substring of field \textit{n} (1-based).
%
If \texttt{-v} is provided, then returns those records without
\textit{str} a substring of field \textit{n}.
Records are drawn from file \textit{file} if it is supplied. If not, they
are taken from standard input.

%----------------------------------------------------------------------------
\subsection{Merge two CSV files}
%----------------------------------------------------------------------------
Usage:
\begin{quote}
   \texttt{csvmerge} \textit{file1 m1 \ldots{} mj file2 n1 \ldots{} nk}
\end{quote}
The files \textit{file1} and \textit{file2} must have the same number
of records.
This command merges corresponding records from the two files and outputs
them on standard output.
The merged records are composed from 
fields \textit{m1 \ldots{} mj} in the records in \textit{file1} and 
fields \textit{n1 \ldots{} nk} in the records in \textit{file2}.
If \textit{j} = 0, all fields of  \textit{file1} records are used.
If \textit{k} = 0, all fields of  \textit{file2} records are used.
Fields are numbered starting from 1.

%----------------------------------------------------------------------------
\subsection{Project out fields of CSV records}
%----------------------------------------------------------------------------
Usage:
\begin{quote}
  \texttt{csvproj} [\texttt{-v}] \textit{n1 \ldots{} nk} [\textit{file}]
\end{quote}
Build new records from fields \textit{n1 \ldots{} nk} of the input
records and output to standard output.  Input records are drawn from
file \textit{file} if it is supplied. If not, they are taken from
standard input.  If option \texttt{-v} is supplied, then all fields
but \textit{n1 \ldots{} nk} are used to build the output records.
Fields are numbered starting from 1.

%----------------------------------------------------------------------------
%\subsection{Intersecting CSV files}
%----------------------------------------------------------------------------
Usage:
\begin{quote}
  \texttt{csvisect} \textit{file1} \textit{file2}
\end{quote}
Print on standard output those records that occur in both
\textit{file1} and \textit{file2}.  Comparison of records currently
just uses string equality, so it is sensitive to whitespace between
record fields. 


%============================================================================
%\section{Known limitations}
%============================================================================
% \begin{enumerate}
% \item 
% \end{enumerate}

%============================================================================
%\section{Known problems}
%============================================================================

% \begin{enumerate}
% \item 
% \end{enumerate}

%============================================================================
\section{Missing Documentation}
%============================================================================
The current Victor has several features that are not properly documented
yet in this manual.  These include:
\begin{itemize}
\item Support for outputing VCs for proof using the Isabelle/HOL
  theorem prover.

  The current release includes some preliminary code for this.
  Improved code has been developed and is waiting to be merged in.
\end{itemize}


%============================================================================
\section{Future developments}
%============================================================================

Here are some ideas for future next steps.  Currently there are no
definite plans for any of these to happen.  If you are a Victor user
and might be interested in any of these, please get in touch.  Or, if
you would like to take on a project to add any of these features
yourself, please get in touch too.

\begin{enumerate}
\item \textbf{Improvement of support for proving VCs using interactive
    theorem provers.}

  The current Victor has some preliminary code for interfacing to
  Isabelle/HOL.  Fabian Immler at TU M\"unchen developed this further
  in 2010 and Secunet\footnote{\url{http://www.secunet.com/}} took
  some interest in this interface.  (Secunet since have developed
  their own \spark{} \fdl{} Isabelle/HOL interface.)
    
  Interfaces to other theorem provers such as PVS and HOL Light would
  be interesting to explore.

  Continued work on interfaces almost-certainly ought to exploit the
  incremental prover driver in order to write out a single prover
  input file for each \spark{} unit.

\item \textbf{An API interface for \zthree}.  This could offer
  improved performance and increased functionality.

\item \textbf{A native input language Alt-Ergo interface.} This could
  offer improved performance and increased functionality, especially
  as the Alt-Ergo team currently appear to be emphasising support for
  its native input language.  over \smtlib{} 1.2 or 2.

\item \textbf{Exploitation of \zthree{} \smtlib 2{} extensions for arrays and
  records.}  Again, a benefit could be improved performance.

\item \textbf{Exploitation of the bit-vector handling capabilities of \smt{}
  solvers.}  As a pre-processing step, this would involve recovering
  finite range information for integer-typed constants, functions and
  variables.

\item \textbf{Exploration of counter-example generation.}  With the
  usual high number of quantified hypotheses and rules, \smt{} solvers
  virtually always report an \emph{unknown} result rather than a
  \emph{sat} result when proof fails.

  How could \smt{} solvers be persuaded to still return some tentative
  counter-example information, perhaps with some indication of which
  quantified assumptions were not fully examined and potentially could
  still refute the counter-example?

  The riposte
  project\footnote{\url{https://forge.open-do.org/projects/riposte/}}
  has been exploring counter-example generation using answer-set
  programming.  It would interesting to compare counter-examples
  produced by these two alternative methods.

\end{enumerate}


\end{document}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
